ds:x:Id fp Type, da:k:Knd fp Type, i:Id, es:ES.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e1, e2:E. loc(e2) = i  es-hist{i:l}(es;e1;e2)  event-info(ds;da) List) 

latex

Definitions	es-info(es;e), t  T, event-info(ds;da), x:A. B(x), map(f;as), S  T, P  Q, es-hist{i:l}(es;e1;e2), x. t(x), a:A fp B(a), Knd, ES, Top, IdDeq, f(x)?z, vartype(i;x), kind(e), KindDeq, valtype(e), Prop, [e, e'], loc(e), Id, E, b, False, A
Lemmas	es-info wf, es-loc-pred, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, Knd wf, fpf wf, es-interval wf2, map wf, event-info wf, es-E wf, Id wf, es-loc wf